Inference at * 
Iof proof for Lemma length-lastn:


  A:Type, L:(A List), n:. (n  ||L||)  (||lastn(n;L)|| = n) 

latex

 by ((Unfold `lastn` 0) 
CollapseTHEN (Auto)) 

latex

C1: 

C1: 1. A : Type
C1: 2. L : A List
C1: 3. n : 
C1: 4. n  ||L||
C1:   ||nth_tl(||L|| - n;L)|| = n
C.

Definitions	lastn(n;L), A, False, P  Q, A  B, S  T, |g|, , {x:A| B(x)} , ||as||, x:A. B(x), x:AB(x), , type List, s = t, t  T, Type
Lemmas	le wf, length wf1, nat wf